Trở thành quy chuẩn vào giữa thế kỉ, danh sách các bài toán của Hilbert cũng là một dạng tuyên ngôn, mở ra con đường cho sự phát triển của trường phái hình thức hóa, một trong ba trường phái lớn của toán học trong thế kỉ 20. Theo những người thuộc trường phái hình thức hóa, toán học là một trò chơi với các ký hiệu bị làm mất đi ý nghĩa riêng theo những quy luật mang tính hình thức được đồng ý trước. Do vậy nó là một hoạt động độc lập của suy nghĩ. Tuy vậy vẫn có nhiều người nghi ngờ về quan điểm của chính Hilbert liệu là chỉ đơn giản như vậy theo những người theo chủ nghĩa hình thức.

Chương trình của Hilbert

Vào năm 1920 ông đề nghị một dự án nghiên cứu rõ ràng (về metamathematics, như là nó được gọi) mà sau đó được biết đến như là chương trình Hilbert. Ông muốn toán học phải được hệ thống hóa trên một nền tảng logic vững chắc và đầy đủ. Ông tin rằng về nguyên tắc điều này có thể làm được, bằng cách chứng minh rằng:

1. tất cả toán học có thể suy ra từ một hệ thống hữu hạn các tiên đề được chọn ra một cách đúng đắn; và
2. rằng một hệ thống tiên đề như vậy là có thể chứng minh được tính nhất quán của nó.

Ông dường như là có cả những lý do kỹ thuật và triết học trong việc hình thức hóa đề nghị này. Nó khẳng định về sự không thích của ông đối với thứ được biết là ignorabimus, vẫn là một vấn đề tồn tại trong suy nghĩ của người Đức trong thời đó, và suy ngược về nguồn gốc từ Emil du Bois-Reymond.

Chương trình này vẫn được công nhận là nổi tiếng nhất về triết học của toán học, nơi mà nó thường được gọi là hình thức hóa. Ví dụ, nhóm Bourbaki lựa cách đi theo kiểu trên-xuống đủ cho những yêu cầu cho dự án đôi của họ (a) một bộ bách khoa toàn thư có tính nền tảng và (b) giúp cho phương pháp tiên đề như là một công cụ nghiên cứu. Cách tiếp cận này đã thành công và có ảnh hưởng liên quan đến các công trình của Hilbert trong đại số và giải tích hàm, nhưng thất bại trong cách tiếp cận tương tự với vật lý và logic của ông.

Công trình của Gödel

Hilbert và các nhà toán học tài năng làm việc cùng nhóm với ông đã dành hết tâm huyết cho dự án này. Cố gắng của ông để ủng hộ nền toán học được xây trên các tiên đề và các nguyên lý xác định trước, làm loại bỏ những bất định trong lý thuyết, tuy nhiên đã thất bại.

Gödel đã chứng minh rằng bất kì một hệ thống hình thức không chứa đựng mâu thuẫn nào,đủ phức tạp để chứa đụng ít nhất là số học, không thể chứng minh sự toàn vẹn của nó bằng các tiên đề của chính nó. Vào năm 1931 định lý bất toàn của Gödel đã cho thấy rằng chương trình vĩ đại của Hilbert là không thể như đã phát biểu. Điểm thứ hai không thể kết nối một cách hợp lý với điểm thứ nhất, miễn là hệ thống tiên đề thực sự là hữu hạn.

Dù sao đi nữa, định lý bất toàn không nói lên gì cả về việc biểu diễn sự toàn vẹn của toán học bằng một hệ thống hình thức hóa khác. Những thành tựu sau đó của lý thuyết chứng minh ít nhất là làm rõ thêm sự nhất quán khi nó liên hệ đến các lý thuyết nằm trong tầm quan tâm chung của các nhà toán học. Công trình của Hilbert đã khởi đầu cho logic trên hướng đi làm rõ này; sự cần thiết hiểu rõ công trình của Gödel sau này dẫn đến sự phát triển của lý thuyết đệ quy và sau đó là logic toán học như là một ngành độc lập trong thập kỉ 1930-1940. Cơ sở cho lý thuyết khoa học máy tính sau này, trong các công trình của Alonzo Church và Alan Turing cũng phát triển trục tiếp từ 'tranh luận' này.